$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $Q$:($x$:$A$$\rightarrow$$B$($x$)$\rightarrow$Type).
\\[0ex]($\forall$$x$:$A$. $\exists$$y$:$B$($x$). $Q$($x$,$y$)) $\Rightarrow$ ($\exists$$f$:$x$:$A$$\rightarrow$$B$($x$). ($\forall$$x$:$A$. $Q$($x$,$f$($x$))))